00100	(GIVEAX GE3
00200	 ((FORALL X)
00300	  ((FORALL Y)
00400	   ((FORALL Z)
00500	    (IMPLIES
00600	     (AND (GEQ X Y) (GEQ Y Z))
00700	     (GEQ X Z))))))
00800	
00900	(GIVEAX GE2 ((FORALL X) (GEQ (S X) X)))
01000	
01100	(GIVEAX GE1 ((FORALL X) (GEQ X X)))
01200	
01300	(GIVEAX NOTALL
01400	 (IMPLIES
01500	  (NOT ((FORALL X) (G X)))
01600	  ((THEREEXISTS X) (NOT (G X)))))
01700	
01800	(GIVEAX EXTENSION
01900	 ((FORALL U)
02000	  ((FORALL V)
02100	   (EQUIVALENT
02200	    (EQUAL U V)
02300	    ((FORALL X)
02400	     (EQUIVALENT (MEMBER X U) (MEMBER X V)))))))
02500	
02600	(GIVEAX PAIRING
02700	 ((FORALL U)
02800	  ((FORALL V)
02900	   ((THEREEXISTS W)
03000	    (AND (MEMBER U W) (MEMBER V W))))))
03100	
03200	(GIVEAX UNIONS
03300	 ((FORALL U)
03400	  ((THEREEXISTS V)
03500	   ((FORALL X)
03600	    (EQUIVALENT
03700	     (MEMBER X V)
03800	     ((THEREEXISTS Y)
03900	      (AND (MEMBER X Y) (MEMBER Y U))))))))
04000	
04100	(GIVEAX POWERS
04200	 ((FORALL U)
04300	  ((THEREEXISTS V)
04400	   ((FORALL X) (EQUIVALENT (MEMBER X V) (X (⊂ U)))))))
04500	
04600	(GIVESCHM FREGE
04700	 ((LAMBDA PRED)
04800	  ((THEREEXISTS Y)
04900	   ((FORALL X) (EQUIVALENT (MEMBER X Y) (PRED X))))))
05000	
05100	(GIVESCHM INDUCTION
05200	 ((LAMBDA PRED)
05300	  (IMPLIES
05400	   (AND (PRED 0) (IMPLIES (PRED N) (PRED (S N))))
05500	   ((FORALL N) (PRED N)))))
05600	
05700	
05800	(PROOF P1) 
05900	1 	(ASS P)
06000	2 	(DED 1 1)
06100	
06200	(PROOF P2) 
06300	1 	(ASS P)
06400	2 	(ASS Q)
06500	3 	(DED 2 1)
06600	4 	(DED 3 2)
06700	
06800	(PROOF P3) 
06900	1 	(ASS P)
07000	2 	(ASS (IMPLIES P Q))
07100	3 	(MP 1 2)
07200	4 	(DED 3 2)
07300	5 	(DED 4 1)
07400	
07500	(PROOF P4) 
07600	1 	(ASS (IMPLIES P Q))
07700	2 	(ASS (IMPLIES Q R))
07800	3 	(ASS P)
07900	4 	(MP 1 3)
08000	5 	(MP 2 4)
08100	6 	(DED 5 3)
08200	7 	(DED 6 2)
08300	8 	(DED 7 1)
08400	
08500	(PROOF P5) 
08600	1 	(ASS (IMPLIES Q R))
08700	2 	(ASS (IMPLIES P Q))
08800	3 	(ASS P)
08900	4 	(MP 2 3)
09000	5 	(MP 1 4)
09100	6 	(DED 5 3)
09200	7 	(DED 6 2)
09300	8 	(DED 7 1)
09400	
09500	(PROOF P6) 
09600	1 	(ASS (IMPLIES P (IMPLIES Q R)))
09700	2 	(ASS (IMPLIES P Q))
09800	3 	(ASS P)
09900	4 	(MP 2 3)
10000	5 	(MP 1 3)
10100	6 	(MP 4 5)
10200	7 	(DED 6 3)
10300	8 	(DED 7 2)
10400	9 	(DED 8 1)
10500	
10600	(PROOF P7) 
10700	1 	(ASS (IMPLIES (IMPLIES P Q) (IMPLIES P R)))
10800	2 	(ASS P)
10900	3 	(ASS Q)
11000	4 	(DED 3 2)
11100	5 	(MP 1 4)
11200	6 	(MP 2 5)
11300	7 	(DED 6 3)
11400	8 	(DED 7 2)
11500	9 	(DED 8 1)
11600	
11700	(PROOF P8) 
11800	1 	(ASS (IMPLIES P (IMPLIES Q R)))
11900	2 	(ASS Q)
12000	3 	(ASS P)
12100	4 	(MP 1 3)
12200	5 	(MP 2 4)
12300	6 	(DED 5 2)
12400	7 	(DED 6 3)
12500	8 	(DED 7 1)
12600	
12700	(PROOF P9) 
12800	1 	(ASS (IMPLIES P (IMPLIES P Q)))
12900	2 	(ASS P)
13000	3 	(MP 1 2)
13100	4 	(MP 2 3)
13200	5 	(DED 4 2)
13300	6 	(DED 5 1)
13400	
13500	(PROOF P10) 
13600	1 	(ASS (IMPLIES P (IMPLIES P Q)))
13700	2 	(ASS (IMPLIES Q P))
13800	3 	(ASS (NOT P))
13900	4 	(ASS Q)
14000	5 	(MP 2 4)
14100	6 	(NE 3 5)
14200	7 	(DED 6 4)
14300	8 	(NI 7)
14400	9 	(ASS (IMPLIES (IMPLIES P Q) Q))
14500	10 	(TAUT (NOT (IMPLIES P Q)) 9 8)
14600	11 	(TAUT P 10)
14700	12 	(NE 3 11)
14800	13 	(DED 12 3)
14900	14 	(NI 13)
15000	15 	(DNE 14)
15100	16 	(DED 15 2)
15200	17 	(DED 16 9)
15300	
15400	(PROOF EAAE) 
15500	1 	(ASS ((THEREEXISTS Y) ((FORALL X) (F X Y))))
15600	2 	(ES 1 A)
15700	3 	(US 2 X)
15800	4 	(EG 3 A Y)
15900	5 	(UG 4 X)
16000	6 	(DED 5 1)
16100	
16200	(PROOF ANEN) 
16300	1 	(ASS ((FORALL X) (F X)))
16400	2 	(ASS ((THEREEXISTS X) (NOT (F X))))
16500	3 	(ES 2 A)
16600	4 	(US 1 A)
16700	5 	(NE 3 4)
16800	6 	(DED 5 2)
16900	7 	(NI 6)
17000	8 	(DED 7 1)
17100	
17200	(PROOF ALLGE) 
17300	1 	(USESCHM INDUCTION ((LAMBDA X) (GEQ X 0)))
17400	2 	(USEAX GE1)
17500	3 	(US 2 0)
17600	4 	(USEAX GE2)
17700	5 	(US 4 N)
17800	6 	(ASS (GEQ N 0))
17900	7 	(USEAX GE3)
18000	8 	(US 7 (S N))
18100	9 	(US 8 N)
18200	10 	(US 9 0)
18300	11 	(AI 5 6)
18400	12 	(MP 10 11)
18500	13 	(DED 12 6)
18600	14 	(AI 3 13)
18700	15 	(MP 1 14)
18800	
18900	(PROOF EXM) 
19000	1 	(ASS (NOT (OR A (NOT A))))
19100	2 	(ASS A)
19200	3 	(OI 2 (NOT A))
19300	4 	(NE 1 3)
19400	5 	(DED 4 2)
19500	6 	(NI 5)
19600	7 	(OI A 6)
19700	8 	(NE 1 7)
19800	9 	(DED 8 1)
19900	10 	(NI 9)
20000	11 	(DNE 10)
20100	
20200	(PROOF JMC) 
20300	1 	(ASS ((FORALL X) (G X)))
20400	2 	(ASS (G X))
20500	3 	(US 1 Y)
20600	4 	(DED 3 2)
20700	5 	(UG 4 Y)
20800	6 	(EG 5 X)
20900	7 	(DED 6 1)
21000	8 	(USEAX NOTALL)
21100	9 	(ASS (NOT ((FORALL X) (G X))))
21200	10 	(MP 8 9)
21300	11 	(ES 10 B)
21400	12 	(ASS (G B))
21500	13 	(NE 12 11)
21600	14 	(ASS (NOT (G Y)))
21700	15 	(DED 13 14)
21800	16 	(NI 15)
21900	17 	(DNE 16)
22000	18 	(DED 17 12)
22100	19 	(UG 18 Y)
22200	20 	(EG 19 (CONS B X))
22300	21 	(DED 20 9)
22400	22 	(ALT 7 21)